Inference at * 1 0 
Iof proof for Lemma assert of le int:



1. x : 
2. y : 
  ((y <z x))  ((y < x)) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 3:n, 4:n, 5:n, 6:n} 

latex

 1: .....wf..... NILNIL

 1:   ((y <z x))  
 2: .....wf..... NILNIL

 2:   ((y <z x))  
 3: .....wf..... NILNIL

 3:   ((y < x))  
 4: .....wf..... NILNIL

 4:   y <z x  
 5: .....wf..... NILNIL

 5:   ((y < x)) = ((y < x))
 6: 

 6:   ((y <z x))  ((y < x))
 .

Definitions	t  T, x:A  B(x), Type, , f(a), s = t, x:AB(x), , a < b, A, i <z j, b, b, , x:A. B(x), P  Q, P  Q, P  Q, P  Q
Lemmas	assert of bnot, iff functionality wrt iff